\begin{tabbing}
recognizer{-}p(${\it es}$;$T$;$A$;$P$;$k$;$i$;$r$;$x$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=alle{-}at(${\it es}$;$i$;$e$.(es{-}kind(${\it es}$; $e$) = $k$ $\in$ Knd) $\Rightarrow$ (es{-}valtype(${\it es}$; $e$) $\subseteq$r $T$))\+
\\[0ex]\& (es{-}vartype(${\it es}$; $i$; $x$) $\subseteq$r $A$)
\\[0ex]\& es{-}dtype(${\it es}$;$i$;$r$;$\mathbb{B}$)
\\[0ex]\& alle{-}at(${\it es}$;$i$;$e$.($\uparrow$es{-}first(${\it es}$; $e$)) $\Rightarrow$ (es{-}when(${\it es}$; $r$; $e$) = ff $\in$ $\mathbb{B}$))
\\[0ex]\& \=alle{-}at(${\it es}$;$i$;$e$.($\uparrow$es{-}after(${\it es}$; $r$; $e$))\+
\\[0ex]$\Leftarrow\!\Rightarrow$ ($\exists$\=${\it e'}$:es{-}E(${\it es}$)\+
\\[0ex]((es{-}le(${\it es}$;${\it e'}$;$e$) \& es{-}kind(${\it es}$; ${\it e'}$) = $k$ $\in$ Knd)
\\[0ex]c$\wedge$ ($\uparrow$($P$(es{-}when(${\it es}$; $x$; ${\it e'}$),es{-}val(${\it es}$; ${\it e'}$)))))))
\-\-\-
\end{tabbing}